On the intuitionistic force of classical search
Identifieur interne : 009F89 ( Main/Exploration ); précédent : 009F88; suivant : 009F90On the intuitionistic force of classical search
Auteurs : E. Ritter [Royaume-Uni] ; D. Pym [Royaume-Uni] ; L. Wallen [Royaume-Uni]Source :
- Theoretical computer science [ 0304-3975 ] ; 2000.
Descripteurs français
- Pascal (Inist)
English descriptors
- KwdEn :
Abstract
The combinatorics of classical propositional logic lies at the heart of both local and global methods of proof-search enabling the achievement of least-commitment search. Extension of such methods to the predicate calculus, or to non-classical systems, presents us with the problem of recovering this least-commitment principle in the context of non-invertible rules. One successful approach is to view the non-classical logic as a perturbation on search in classical logic and characterize when a least-commitment (classical) search yields sufficient evidence for provability in the (non-classical) logic. This technique has been successfully applied to both local and global methods at the cost of subsidiary searches and is the analogue of the standard treatment of quantifiers via skolemization and unification. In this paper, we take a type-theoretic view of this approach for the case in which the non-classical logic is intuitionistic. We develop a system of realizers (proof-objects) for sequents in classical propositional logic (the types) by extending Parigot's λμ-calculus, a system of realizers for classical free deduction (cf. natural deduction). Our treatment of disjunction exploits directly the multiple-conclusioned form of LK as opposed to the single-conclusioned form of LJ. Consequently, it requires the addition of another binding operator, called v, to λμ. This choice is motivated by our concern to reflect the properties of classical proof-search in the system of realizers. Using this framework, we illustrate the sense in which intuitionistic search can be viewed as a perturbation on classical search. As an application, we develop a proof procedure based on the natural extension of the notion of uniform proof to the multiple-conclusioned classical sequent calculus Harrop fragment of intuitionistic logic. This paper develops the proof-theoretic aspects of the approach.
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream PascalFrancis, to step Corpus: 000A75
- to stream PascalFrancis, to step Curation: 000007
- to stream PascalFrancis, to step Checkpoint: 000986
- to stream Main, to step Merge: 00A592
- to stream Main, to step Curation: 009F89
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">On the intuitionistic force of classical search</title><author><name sortKey="Ritter, E" sort="Ritter, E" uniqKey="Ritter E" first="E." last="Ritter">E. Ritter</name><affiliation wicri:level="4"><inist:fA14 i1="01"><s1>School of Computer Science, University of Birmingham</s1><s2>Birmingham, B15 2TT</s2><s3>GBR</s3><sZ>1 aut.</sZ></inist:fA14><country>Royaume-Uni</country><placeName><settlement type="city">Birmingham</settlement><region type="country">Angleterre</region><region type="région" nuts="1">Midlands de l'Ouest</region></placeName><orgName type="university">Université de Birmingham</orgName></affiliation></author><author><name sortKey="Pym, D" sort="Pym, D" uniqKey="Pym D" first="D." last="Pym">D. Pym</name><affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Department of Computer Science, Queen Mary & Westfield College, University of London. Mile End Road</s1><s2>London, E1 4NS</s2><s3>GBR</s3><sZ>2 aut.</sZ></inist:fA14><country>Royaume-Uni</country><wicri:noRegion>London, E1 4NS</wicri:noRegion></affiliation></author><author><name sortKey="Wallen, L" sort="Wallen, L" uniqKey="Wallen L" first="L." last="Wallen">L. Wallen</name><affiliation wicri:level="1"><inist:fA14 i1="03"><s1>Programming Research Group, Computing Laboratory, Oxford University, 8-11 Keble Road</s1><s2>Oxford, OX1 3QD</s2><s3>GBR</s3><sZ>3 aut.</sZ></inist:fA14><country>Royaume-Uni</country><wicri:noRegion>Oxford, OX1 3QD</wicri:noRegion></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">INIST</idno><idno type="inist">00-0103172</idno><date when="2000">2000</date><idno type="stanalyst">PASCAL 00-0103172 INIST</idno><idno type="RBID">Pascal:00-0103172</idno><idno type="wicri:Area/PascalFrancis/Corpus">000A75</idno><idno type="wicri:Area/PascalFrancis/Curation">000007</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000986</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000986</idno><idno type="wicri:doubleKey">0304-3975:2000:Ritter E:on:the:intuitionistic</idno><idno type="wicri:Area/Main/Merge">00A592</idno><idno type="wicri:Area/Main/Curation">009F89</idno><idno type="wicri:Area/Main/Exploration">009F89</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">On the intuitionistic force of classical search</title><author><name sortKey="Ritter, E" sort="Ritter, E" uniqKey="Ritter E" first="E." last="Ritter">E. Ritter</name><affiliation wicri:level="4"><inist:fA14 i1="01"><s1>School of Computer Science, University of Birmingham</s1><s2>Birmingham, B15 2TT</s2><s3>GBR</s3><sZ>1 aut.</sZ></inist:fA14><country>Royaume-Uni</country><placeName><settlement type="city">Birmingham</settlement><region type="country">Angleterre</region><region type="région" nuts="1">Midlands de l'Ouest</region></placeName><orgName type="university">Université de Birmingham</orgName></affiliation></author><author><name sortKey="Pym, D" sort="Pym, D" uniqKey="Pym D" first="D." last="Pym">D. Pym</name><affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Department of Computer Science, Queen Mary & Westfield College, University of London. Mile End Road</s1><s2>London, E1 4NS</s2><s3>GBR</s3><sZ>2 aut.</sZ></inist:fA14><country>Royaume-Uni</country><wicri:noRegion>London, E1 4NS</wicri:noRegion></affiliation></author><author><name sortKey="Wallen, L" sort="Wallen, L" uniqKey="Wallen L" first="L." last="Wallen">L. Wallen</name><affiliation wicri:level="1"><inist:fA14 i1="03"><s1>Programming Research Group, Computing Laboratory, Oxford University, 8-11 Keble Road</s1><s2>Oxford, OX1 3QD</s2><s3>GBR</s3><sZ>3 aut.</sZ></inist:fA14><country>Royaume-Uni</country><wicri:noRegion>Oxford, OX1 3QD</wicri:noRegion></affiliation></author></analytic><series><title level="j" type="main">Theoretical computer science</title><title level="j" type="abbreviated">Theor. comput. sci.</title><idno type="ISSN">0304-3975</idno><imprint><date when="2000">2000</date></imprint></series></biblStruct></sourceDesc><seriesStmt><title level="j" type="main">Theoretical computer science</title><title level="j" type="abbreviated">Theor. comput. sci.</title><idno type="ISSN">0304-3975</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Intuitionistic logic</term><term>Lambda calculus</term><term>Lambda mu calculus</term><term>Logic</term><term>Logical programming</term><term>Proof search</term><term>Substitution</term><term>Uniform proof</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Logique</term><term>Programmation logique</term><term>Lambda calcul</term><term>Substitution</term><term>Recherche preuve</term><term>Calcul lambda mu</term><term>Logique intuitionniste</term><term>Preuve uniforme</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">The combinatorics of classical propositional logic lies at the heart of both local and global methods of proof-search enabling the achievement of least-commitment search. Extension of such methods to the predicate calculus, or to non-classical systems, presents us with the problem of recovering this least-commitment principle in the context of non-invertible rules. One successful approach is to view the non-classical logic as a perturbation on search in classical logic and characterize when a least-commitment (classical) search yields sufficient evidence for provability in the (non-classical) logic. This technique has been successfully applied to both local and global methods at the cost of subsidiary searches and is the analogue of the standard treatment of quantifiers via skolemization and unification. In this paper, we take a type-theoretic view of this approach for the case in which the non-classical logic is intuitionistic. We develop a system of realizers (proof-objects) for sequents in classical propositional logic (the types) by extending Parigot's λμ-calculus, a system of realizers for classical free deduction (cf. natural deduction). Our treatment of disjunction exploits directly the multiple-conclusioned form of LK as opposed to the single-conclusioned form of LJ. Consequently, it requires the addition of another binding operator, called v, to λμ. This choice is motivated by our concern to reflect the properties of classical proof-search in the system of realizers. Using this framework, we illustrate the sense in which intuitionistic search can be viewed as a perturbation on classical search. As an application, we develop a proof procedure based on the natural extension of the notion of uniform proof to the multiple-conclusioned classical sequent calculus Harrop fragment of intuitionistic logic. This paper develops the proof-theoretic aspects of the approach.</div></front></TEI><affiliations><list><country><li>Royaume-Uni</li></country><region><li>Angleterre</li><li>Midlands de l'Ouest</li></region><settlement><li>Birmingham</li></settlement><orgName><li>Université de Birmingham</li></orgName></list><tree><country name="Royaume-Uni"><region name="Angleterre"><name sortKey="Ritter, E" sort="Ritter, E" uniqKey="Ritter E" first="E." last="Ritter">E. Ritter</name></region><name sortKey="Pym, D" sort="Pym, D" uniqKey="Pym D" first="D." last="Pym">D. Pym</name><name sortKey="Wallen, L" sort="Wallen, L" uniqKey="Wallen L" first="L." last="Wallen">L. Wallen</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 009F89 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 009F89 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= Pascal:00-0103172
|texte= On the intuitionistic force of classical search
}}
| This area was generated with Dilib version V0.6.33. |  |